Structure quoteTheory
signature quoteTheory =
sig
type thm = Thm.thm
(* Definitions *)
val Empty_vm : thm
val End_idx : thm
val Left_idx : thm
val Node_vm : thm
val Right_idx : thm
val index_TY_DEF : thm
val index_case_def : thm
val index_compare_curried_def : thm
val index_compare_tupled_primitive_def : thm
val index_lt_def : thm
val index_repfns : thm
val index_size_def : thm
val quote0_def : thm
val quote1_def : thm
val quote2_def : thm
val quote3_def : thm
val quote4_def : thm
val varmap_TY_DEF : thm
val varmap_case_def : thm
val varmap_find_curried_def : thm
val varmap_find_tupled_primitive_def : thm
val varmap_repfns : thm
val varmap_size_def : thm
(* Theorems *)
val compare_index_equal : thm
val compare_list_index : thm
val datatype_index : thm
val datatype_varmap : thm
val index_11 : thm
val index_Axiom : thm
val index_case_cong : thm
val index_compare_def : thm
val index_compare_ind : thm
val index_distinct : thm
val index_induction : thm
val index_nchotomy : thm
val varmap_11 : thm
val varmap_Axiom : thm
val varmap_case_cong : thm
val varmap_distinct : thm
val varmap_find_def : thm
val varmap_find_ind : thm
val varmap_induction : thm
val varmap_nchotomy : thm
val quote_grammars : type_grammar.grammar * term_grammar.grammar
(*
[prelim] Parent theory of "quote"
[Empty_vm] Definition
|- Empty_vm = quote3
[End_idx] Definition
|- End_idx = quote2
[Left_idx] Definition
|- Left_idx = quote0
[Node_vm] Definition
|- Node_vm = quote4
[Right_idx] Definition
|- Right_idx = quote1
[index_TY_DEF] Definition
|- ?rep.
TYPE_DEFINITION
(\a0.
!'index'.
(!a0.
(?a.
(a0 =
(\a.
ind_type$CONSTR 0 (@x. T)
(FCONS a (\n. ind_type$BOTTOM))) a) /\ 'index' a) \/
(?a.
(a0 =
(\a.
ind_type$CONSTR (SUC 0) (@x. T)
(FCONS a (\n. ind_type$BOTTOM))) a) /\ 'index' a) \/
(a0 =
ind_type$CONSTR (SUC (SUC 0)) (@x. T)
(\n. ind_type$BOTTOM)) ==>
'index' a0) ==>
'index' a0) rep
[index_case_def] Definition
|- (!f f1 v a. index_case f f1 v (Left_idx a) = f a) /\
(!f f1 v a. index_case f f1 v (Right_idx a) = f1 a) /\
!f f1 v. index_case f f1 v End_idx = v
[index_compare_curried_def] Definition
|- !x x1. index_compare x x1 = index_compare_tupled (x,x1)
[index_compare_tupled_primitive_def] Definition
|- index_compare_tupled =
WFREC
(@R.
WF R /\ (!m' n'. R (n',m') (Left_idx n',Left_idx m')) /\
!m' n'. R (n',m') (Right_idx n',Right_idx m'))
(\index_compare_tupled a.
case a of
(Left_idx n',Left_idx m') -> I (index_compare_tupled (n',m'))
|| (Left_idx n',Right_idx m'') -> I LESS
|| (Left_idx n',End_idx) -> I GREATER
|| (Right_idx n'',Left_idx m'''') -> I GREATER
|| (Right_idx n'',Right_idx m''') ->
I (index_compare_tupled (n'',m'''))
|| (Right_idx n'',End_idx) -> I GREATER
|| (End_idx,Left_idx v12) -> I LESS
|| (End_idx,Right_idx v13) -> I LESS
|| (End_idx,End_idx) -> I EQUAL)
[index_lt_def] Definition
|- !i1 i2. index_lt i1 i2 = (index_compare i1 i2 = LESS)
[index_repfns] Definition
|- (!a. mk_index (dest_index a) = a) /\
!r.
(\a0.
!'index'.
(!a0.
(?a.
(a0 =
(\a.
ind_type$CONSTR 0 (@x. T) (FCONS a (\n. ind_type$BOTTOM)))
a) /\ 'index' a) \/
(?a.
(a0 =
(\a.
ind_type$CONSTR (SUC 0) (@x. T)
(FCONS a (\n. ind_type$BOTTOM))) a) /\ 'index' a) \/
(a0 =
ind_type$CONSTR (SUC (SUC 0)) (@x. T) (\n. ind_type$BOTTOM)) ==>
'index' a0) ==>
'index' a0) r =
(dest_index (mk_index r) = r)
[index_size_def] Definition
|- (!a. index_size (Left_idx a) = 1 + index_size a) /\
(!a. index_size (Right_idx a) = 1 + index_size a) /\
(index_size End_idx = 0)
[quote0_def] Definition
|- quote0 =
(\a.
mk_index
((\a. ind_type$CONSTR 0 (@x. T) (FCONS a (\n. ind_type$BOTTOM)))
(dest_index a)))
[quote1_def] Definition
|- quote1 =
(\a.
mk_index
((\a. ind_type$CONSTR (SUC 0) (@x. T) (FCONS a (\n. ind_type$BOTTOM)))
(dest_index a)))
[quote2_def] Definition
|- quote2 =
mk_index (ind_type$CONSTR (SUC (SUC 0)) (@x. T) (\n. ind_type$BOTTOM))
[quote3_def] Definition
|- quote3 = mk_varmap (ind_type$CONSTR 0 (@v. T) (\n. ind_type$BOTTOM))
[quote4_def] Definition
|- quote4 =
(\a0 a1 a2.
mk_varmap
((\a0 a1 a2.
ind_type$CONSTR (SUC 0) a0
(FCONS a1 (FCONS a2 (\n. ind_type$BOTTOM)))) a0 (dest_varmap a1)
(dest_varmap a2)))
[varmap_TY_DEF] Definition
|- ?rep.
TYPE_DEFINITION
(\a0'.
!'varmap'.
(!a0'.
(a0' = ind_type$CONSTR 0 (@v. T) (\n. ind_type$BOTTOM)) \/
(?a0 a1 a2.
(a0' =
(\a0 a1 a2.
ind_type$CONSTR (SUC 0) a0
(FCONS a1 (FCONS a2 (\n. ind_type$BOTTOM)))) a0 a1
a2) /\ 'varmap' a1 /\ 'varmap' a2) ==>
'varmap' a0') ==>
'varmap' a0') rep
[varmap_case_def] Definition
|- (!v f. varmap_case v f Empty_vm = v) /\
!v f a0 a1 a2. varmap_case v f (Node_vm a0 a1 a2) = f a0 a1 a2
[varmap_find_curried_def] Definition
|- !x x1. varmap_find x x1 = varmap_find_tupled (x,x1)
[varmap_find_tupled_primitive_def] Definition
|- varmap_find_tupled =
WFREC
(@R.
WF R /\ (!v1 x v2 i1. R (i1,v2) (Right_idx i1,Node_vm x v1 v2)) /\
!v2 x v1 i1. R (i1,v1) (Left_idx i1,Node_vm x v1 v2))
(\varmap_find_tupled a.
case a of
(Left_idx i1',Empty_vm) -> I (@x. T)
|| (Left_idx i1',Node_vm x'' v1'' v2'') ->
I (varmap_find_tupled (i1',v1''))
|| (Right_idx i1,Empty_vm) -> I (@x. T)
|| (Right_idx i1,Node_vm x' v1' v2') -> I (varmap_find_tupled (i1,v2'))
|| (End_idx,Empty_vm) -> I (@x. T)
|| (End_idx,Node_vm x v1 v2) -> I x)
[varmap_repfns] Definition
|- (!a. mk_varmap (dest_varmap a) = a) /\
!r.
(\a0'.
!'varmap'.
(!a0'.
(a0' = ind_type$CONSTR 0 (@v. T) (\n. ind_type$BOTTOM)) \/
(?a0 a1 a2.
(a0' =
(\a0 a1 a2.
ind_type$CONSTR (SUC 0) a0
(FCONS a1 (FCONS a2 (\n. ind_type$BOTTOM)))) a0 a1 a2) /\
'varmap' a1 /\ 'varmap' a2) ==>
'varmap' a0') ==>
'varmap' a0') r =
(dest_varmap (mk_varmap r) = r)
[varmap_size_def] Definition
|- (!f. varmap_size f Empty_vm = 0) /\
!f a0 a1 a2.
varmap_size f (Node_vm a0 a1 a2) =
1 + (f a0 + (varmap_size f a1 + varmap_size f a2))
[compare_index_equal] Theorem
|- !i1 i2. (index_compare i1 i2 = EQUAL) = (i1 = i2)
[compare_list_index] Theorem
|- !l1 l2. (list_compare index_compare l1 l2 = EQUAL) = (l1 = l2)
[datatype_index] Theorem
|- DATATYPE (index Left_idx Right_idx End_idx)
[datatype_varmap] Theorem
|- DATATYPE (varmap Empty_vm Node_vm)
[index_11] Theorem
|- (!a a'. (Left_idx a = Left_idx a') = (a = a')) /\
!a a'. (Right_idx a = Right_idx a') = (a = a')
[index_Axiom] Theorem
|- !f0 f1 f2.
?fn.
(!a. fn (Left_idx a) = f0 a (fn a)) /\
(!a. fn (Right_idx a) = f1 a (fn a)) /\ (fn End_idx = f2)
[index_case_cong] Theorem
|- !M M' f f1 v.
(M = M') /\ (!a. (M' = Left_idx a) ==> (f a = f' a)) /\
(!a. (M' = Right_idx a) ==> (f1 a = f1' a)) /\
((M' = End_idx) ==> (v = v')) ==>
(index_case f f1 v M = index_case f' f1' v' M')
[index_compare_def] Theorem
|- (index_compare End_idx End_idx = EQUAL) /\
(index_compare End_idx (Right_idx v11) = LESS) /\
(index_compare End_idx (Left_idx v10) = LESS) /\
(index_compare (Right_idx v3) End_idx = GREATER) /\
(index_compare (Left_idx v2) End_idx = GREATER) /\
(index_compare (Left_idx n') (Left_idx m') = index_compare n' m') /\
(index_compare (Left_idx n') (Right_idx m') = LESS) /\
(index_compare (Right_idx n') (Right_idx m') = index_compare n' m') /\
(index_compare (Right_idx n') (Left_idx m') = GREATER)
[index_compare_ind] Theorem
|- !P.
P End_idx End_idx /\ (!v11. P End_idx (Right_idx v11)) /\
(!v10. P End_idx (Left_idx v10)) /\ (!v3. P (Right_idx v3) End_idx) /\
(!v2. P (Left_idx v2) End_idx) /\
(!n' m'. P n' m' ==> P (Left_idx n') (Left_idx m')) /\
(!n' m'. P (Left_idx n') (Right_idx m')) /\
(!n' m'. P n' m' ==> P (Right_idx n') (Right_idx m')) /\
(!n' m'. P (Right_idx n') (Left_idx m')) ==>
!v v1. P v v1
[index_distinct] Theorem
|- (!a' a. ~(Left_idx a = Right_idx a')) /\ (!a. ~(Left_idx a = End_idx)) /\
!a. ~(Right_idx a = End_idx)
[index_induction] Theorem
|- !P.
(!i. P i ==> P (Left_idx i)) /\ (!i. P i ==> P (Right_idx i)) /\
P End_idx ==>
!i. P i
[index_nchotomy] Theorem
|- !i. (?i'. i = Left_idx i') \/ (?i'. i = Right_idx i') \/ (i = End_idx)
[varmap_11] Theorem
|- !a0 a1 a2 a0' a1' a2'.
(Node_vm a0 a1 a2 = Node_vm a0' a1' a2') =
(a0 = a0') /\ (a1 = a1') /\ (a2 = a2')
[varmap_Axiom] Theorem
|- !f0 f1.
?fn.
(fn Empty_vm = f0) /\
!a0 a1 a2. fn (Node_vm a0 a1 a2) = f1 a0 a1 a2 (fn a1) (fn a2)
[varmap_case_cong] Theorem
|- !M M' v f.
(M = M') /\ ((M' = Empty_vm) ==> (v = v')) /\
(!a0 a1 a2. (M' = Node_vm a0 a1 a2) ==> (f a0 a1 a2 = f' a0 a1 a2)) ==>
(varmap_case v f M = varmap_case v' f' M')
[varmap_distinct] Theorem
|- !a2 a1 a0. ~(Empty_vm = Node_vm a0 a1 a2)
[varmap_find_def] Theorem
|- (varmap_find End_idx (Node_vm x v1 v2) = x) /\
(varmap_find (Right_idx i1) (Node_vm x v1 v2) = varmap_find i1 v2) /\
(varmap_find (Left_idx i1) (Node_vm x v1 v2) = varmap_find i1 v1) /\
(varmap_find End_idx Empty_vm = @x. T) /\
(varmap_find (Right_idx v6) Empty_vm = @x. T) /\
(varmap_find (Left_idx v5) Empty_vm = @x. T)
[varmap_find_ind] Theorem
|- !P.
(!x v1 v2. P End_idx (Node_vm x v1 v2)) /\
(!i1 x v1 v2. P i1 v2 ==> P (Right_idx i1) (Node_vm x v1 v2)) /\
(!i1 x v1 v2. P i1 v1 ==> P (Left_idx i1) (Node_vm x v1 v2)) /\
P End_idx Empty_vm /\ (!v6. P (Right_idx v6) Empty_vm) /\
(!v5. P (Left_idx v5) Empty_vm) ==>
!v v1. P v v1
[varmap_induction] Theorem
|- !P.
P Empty_vm /\ (!v v0. P v /\ P v0 ==> !a. P (Node_vm a v v0)) ==> !v. P v
[varmap_nchotomy] Theorem
|- !v. (v = Empty_vm) \/ ?a v' v0. v = Node_vm a v' v0
*)
end
HOL 4, Kananaskis-3