equal
deleted
inserted
replaced
854 apply (simp add: QUOT_TYPE_I_fset.thm10) |
854 apply (simp add: QUOT_TYPE_I_fset.thm10) |
855 done |
855 done |
856 |
856 |
857 ML {* |
857 ML {* |
858 fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x) |
858 fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x) |
859 val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}] |
859 val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}, @{const_name "card1"}] |
860 *} |
860 *} |
861 |
861 |
862 ML {* |
862 ML {* |
863 fun build_goal thm constructors lifted_type mk_rep_abs = |
863 fun build_goal thm constructors lifted_type mk_rep_abs = |
864 let |
864 let |
868 let |
868 let |
869 val _ = writeln ("Maybe: " ^ Syntax.string_of_term @{context} t) |
869 val _ = writeln ("Maybe: " ^ Syntax.string_of_term @{context} t) |
870 in |
870 in |
871 if type_of t = lifted_type then mk_rep_abs t else t |
871 if type_of t = lifted_type then mk_rep_abs t else t |
872 end |
872 end |
|
873 handle TYPE _ => t |
873 fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr)) |
874 fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr)) |
874 | build_aux (f $ a) = |
875 | build_aux (f $ a) = |
875 let |
876 let |
876 val (f, args) = strip_comb (f $ a) |
877 val (f, args) = strip_comb (f $ a) |
877 val _ = writeln (Syntax.string_of_term @{context} f) |
878 val _ = writeln (Syntax.string_of_term @{context} f) |
1082 *} |
1083 *} |
1083 ML {* |
1084 ML {* |
1084 val cgoal = cterm_of @{theory} goal |
1085 val cgoal = cterm_of @{theory} goal |
1085 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1086 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1086 *} |
1087 *} |
1087 |
1088 ML fset_defs_sym |
|
1089 prove {* (Thm.term_of cgoal2) *} |
|
1090 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
|
1091 apply (atomize(full)) |
|
1092 apply (rule_tac trueprop_cong) |
|
1093 apply (atomize(full)) |
|
1094 apply (tactic {* foo_tac' @{context} 1 *}) |
|
1095 apply (rule_tac f = "P" in arg_cong) |
|
1096 sorry |
1088 |
1097 |
1089 thm card1_suc |
1098 thm card1_suc |
1090 |
1099 |
1091 ML {* |
1100 ML {* |
1092 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm card1_suc})) |
1101 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm card1_suc})) |
1096 *} |
1105 *} |
1097 ML {* |
1106 ML {* |
1098 val cgoal = cterm_of @{theory} goal |
1107 val cgoal = cterm_of @{theory} goal |
1099 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1108 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1100 *} |
1109 *} |
|
1110 prove {* (Thm.term_of cgoal2) *} |
|
1111 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1101 |
1112 |
1102 |
1113 |
1103 |
1114 |
1104 (* |
1115 (* |
1105 datatype obj1 = |
1116 datatype obj1 = |