Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
QuotMain.thy
changeset 107 ab53ddefc542
parent 106 a250b56e7f2a
child 108 d3a432bd09f0
equal deleted inserted replaced
106:a250b56e7f2a 107:ab53ddefc542 
   378 local_setup {*
 
   378 local_setup {*
 
   379   make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
 
   379   make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
 
   380   make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
 
   380   make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
 
   381   make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
 
   381   make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
 
   382 *}
 
   382 *}
 
       
   383 
       
   384 (*consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t"
 
       
   385 
       
   386 ML {*
 
       
   387     get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"}
 
       
   388  |> fst
 
       
   389  |> Syntax.string_of_term @{context}
 
       
   390  |> writeln
 
       
   391 *}
 
       
   392 
       
   393 local_setup {*
 
       
   394   fn lthy => (Toplevel.program (fn () =>
 
       
   395     make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy
 
       
   396   )) |> snd
 
       
   397 *}
 
       
   398 *)
 
   383 
   399 
   384 term vr'
 
   400 term vr'
 
   385 term ap'
 
   401 term ap'
 
   386 term ap'
 
   402 term ap'
 
   387 thm VR'_def AP'_def LM'_def
 
   403 thm VR'_def AP'_def LM'_def
 
   648   done
 
   664   done
 
   649 
   665 
   650 ML {*
 
   666 ML {*
 
   651   fun mk_rep x = @{term REP_fset} $ x;
 
   667   fun mk_rep x = @{term REP_fset} $ x;
 
   652   fun mk_abs x = @{term ABS_fset} $ x;
 
   668   fun mk_abs x = @{term ABS_fset} $ x;
 
   653   val consts = [@{const_name "Nil"}, @{const_name "append"},
 
   669   val consts = [@{const_name "Nil"}, @{const_name "Cons"},
 
   654                 @{const_name "Cons"}, @{const_name "membship"},
 
   670                 @{const_name "membship"}, @{const_name "card1"},
 
   655                 @{const_name "card1"}]
 
   671                 @{const_name "append"}, @{const_name "fold1"}];
 
   656 *}
 
   672                
       
   673 *}
 
       
   674 
       
   675 ML {* val tm = @{term "x :: 'a list"} *}
 
       
   676 ML {* val ty = exchange_ty @{typ "'a list"} @{typ "'a fset"} (fastype_of tm) *}
 
       
   677 ML {* (fst (get_fun repF @{typ "'a list"} @{typ "'a fset"} @{context} ty)) $ tm *}
 
   657 
   678 
   658 ML {* val qty = @{typ "'a fset"} *}
 
   679 ML {* val qty = @{typ "'a fset"} *}
 
   659 ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *}
 
   680 ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *}
 
   660 ML {* val fall = Const(@{const_name all}, dummyT) *}
 
   681 ML {* val fall = Const(@{const_name all}, dummyT) *}
 
   661 
   682 
   662 ML {*
 
   683 ML {*
 
   663 fun build_goal_term ctxt thm constructors rty qty mk_rep mk_abs =
 
   684 fun needs_lift (rty as Type (rty_s, _)) ty =
 
       
   685   case ty of
 
       
   686     Type (s, tys) =>
 
       
   687       (s = rty_s) orelse (exists (needs_lift rty) tys)
 
       
   688   | _ => false
 
       
   689 
       
   690 *}
 
       
   691 
       
   692 ML {*
 
       
   693 fun build_goal_term lthy thm constructors rty qty =
 
       
   694   let
 
       
   695     fun mk_rep tm =
 
       
   696       let
 
       
   697         val ty = exchange_ty rty qty (fastype_of tm)
 
       
   698       in fst (get_fun repF rty qty lthy ty) $ tm end
 
       
   699 
       
   700     fun mk_abs tm =
 
       
   701       let
 
       
   702         val _ = tracing (Syntax.string_of_term @{context} tm)
 
       
   703         val _ = tracing (Syntax.string_of_typ @{context} (fastype_of tm))
 
       
   704         val ty = exchange_ty rty qty (fastype_of tm) in
 
       
   705       fst (get_fun absF rty qty lthy ty) $ tm end
 
       
   706 
       
   707     fun is_constructor (Const (x, _)) = member (op =) constructors x
 
       
   708       | is_constructor _ = false;
 
       
   709 
       
   710     fun build_aux lthy tm =
 
       
   711       case tm of
 
       
   712       Abs (a as (_, vty, _)) =>
 
       
   713       let
 
       
   714         val (vs, t) = Term.dest_abs a;
 
       
   715         val v = Free(vs, vty);
 
       
   716         val t' = lambda v (build_aux lthy t)
 
       
   717       in
 
       
   718       if (not (needs_lift rty (fastype_of tm))) then t'
 
       
   719       else mk_rep (mk_abs (
 
       
   720         if not (needs_lift rty vty) then t'
 
       
   721         else
 
       
   722           let
 
       
   723             val v' = mk_rep (mk_abs v);
 
       
   724             val t1 = Envir.beta_norm (t' $ v')
 
       
   725           in
 
       
   726             lambda v t1
 
       
   727           end
 
       
   728       ))
 
       
   729       end
 
       
   730     | x =>
 
       
   731       let
 
       
   732         val _ = tracing (">>" ^ Syntax.string_of_term @{context} tm)
 
       
   733         val (opp, tms0) = Term.strip_comb tm
 
       
   734         val tms = map (build_aux lthy) tms0
 
       
   735         val ty = fastype_of tm
 
       
   736       in
 
       
   737         if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false)
 
       
   738           then (list_comb (opp, (hd tms0) :: (tl tms)))
 
       
   739       else if (is_constructor opp andalso needs_lift rty ty) then
 
       
   740           mk_rep (mk_abs (list_comb (opp,tms)))
 
       
   741         else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
 
       
   742             mk_rep(mk_abs(list_comb(opp,tms)))
 
       
   743         else if tms = [] then opp
 
       
   744         else list_comb(opp, tms)
 
       
   745       end
 
       
   746   in
 
       
   747     build_aux lthy (Thm.prop_of thm)
 
       
   748   end
 
       
   749 
       
   750 *}
 
       
   751 
       
   752 ML {*
 
       
   753 fun build_goal_term_old ctxt thm constructors rty qty mk_rep mk_abs =
 
   664   let
 
   754   let
 
   665     fun mk_rep_abs x = mk_rep (mk_abs x);
 
   755     fun mk_rep_abs x = mk_rep (mk_abs x);
 
   666 
   756 
   667     fun is_constructor (Const (x, _)) = member (op =) constructors x
 
   757     fun is_constructor (Const (x, _)) = member (op =) constructors x
 
   668       | is_constructor _ = false;
 
   758       | is_constructor _ = false;
 
   717     build_aux ctxt (Thm.prop_of thm)
 
   807     build_aux ctxt (Thm.prop_of thm)
 
   718   end
 
   808   end
 
   719 *}
 
   809 *}
 
   720 
   810 
   721 ML {*
 
   811 ML {*
 
   722 fun build_goal ctxt thm cons rty qty mk_rep mk_abs =
 
   812 fun build_goal ctxt thm cons rty qty =
 
   723   Logic.mk_equals ((build_goal_term ctxt thm cons rty qty mk_rep mk_abs), (Thm.prop_of thm))
 
   813   Logic.mk_equals ((build_goal_term ctxt thm cons rty qty), (Thm.prop_of thm))
 
   724 *}
 
   814 *}
 
   725 
   815 
   726 ML {*
 
   816 ML {*
 
   727   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
 
   817   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
 
   728 *}
 
   818 *}
 
   729   
   819 
   730 ML {*
 
   820 ML {*
 
   731 m1_novars |> prop_of
 
   821 cterm_of @{theory} (prop_of m1_novars);
 
   732 |> Syntax.string_of_term @{context}
 
   822 cterm_of @{theory} (build_goal_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"});
 
   733 |> writeln; 
   823 cterm_of @{theory} (build_goal_term_old @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs)
 
   734 build_goal_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
 
       
   735 |> Syntax.string_of_term @{context}
 
       
   736 |> writeln
 
       
   737 *}
 
   824 *}
 
   738 
   825 
   739 
   826 
   740 text {*
 
   827 text {*
 
   741   Unabs_def converts a definition given as
 
   828   Unabs_def converts a definition given as
 
   811     ]) 1
 
   898     ]) 1
 
   812 *}
 
   899 *}
 
   813 
   900 
   814 ML {*
 
   901 ML {*
 
   815   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
 
   902   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
 
   816   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
 
   903   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
 
   817   val cgoal = cterm_of @{theory} goal
 
   904   val cgoal = cterm_of @{theory} goal
 
   818   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 
   905   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 
   819 *}
 
   906 *}
 
   820 
   907 
   821 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 
   908 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 
   827   done
 
   914   done
 
   828 
   915 
   829 thm length_append (* Not true but worth checking that the goal is correct *)
 
   916 thm length_append (* Not true but worth checking that the goal is correct *)
 
   830 ML {*
 
   917 ML {*
 
   831   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append}))
 
   918   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append}))
 
   832   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
 
   919   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
 
   833   val cgoal = cterm_of @{theory} goal
 
   920   val cgoal = cterm_of @{theory} goal
 
   834   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 
   921   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 
   835 *}
 
   922 *}
 
   836 prove {* Thm.term_of cgoal2 *}
 
   923 prove {* Thm.term_of cgoal2 *}
 
   837   apply (tactic {* transconv_fset_tac' @{context} *})
 
   924   apply (tactic {* transconv_fset_tac' @{context} *})
 
   838   sorry
 
   925   sorry
 
   839 
   926 
   840 thm m2
 
   927 thm m2
 
   841 ML {*
 
   928 ML {*
 
   842   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
 
   929   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
 
   843   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
 
   930   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
 
   844   val cgoal = cterm_of @{theory} goal
 
   931   val cgoal = cterm_of @{theory} goal
 
   845   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 
   932   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 
   846 *}
 
   933 *}
 
   847 prove {* Thm.term_of cgoal2 *}
 
   934 prove {* Thm.term_of cgoal2 *}
 
   848   apply (tactic {* transconv_fset_tac' @{context} *})
 
   935   apply (tactic {* transconv_fset_tac' @{context} *})
 
   849   done
 
   936   done
 
   850 
   937 
   851 thm list_eq.intros(4)
 
   938 thm list_eq.intros(4)
 
   852 ML {*
 
   939 ML {*
 
   853   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
 
   940   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
 
   854   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
 
   941   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
 
   855   val cgoal = cterm_of @{theory} goal
 
   942   val cgoal = cterm_of @{theory} goal
 
   856   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 
   943   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 
   857   val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2)
 
   944   val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2)
 
   858 *}
 
   945 *}
 
   859 
   946 
   860 (* It is the same, but we need a name for it. *)
 
   947 (* It is the same, but we need a name for it. *)
 
   861 prove zzz : {* Thm.term_of cgoal3 *}
 
   948 prove zzz : {* Thm.term_of cgoal3 *}
 
   862   apply (tactic {* transconv_fset_tac' @{context} *})
 
   949   apply (tactic {* transconv_fset_tac' @{context} *})
 
   863   done
 
   950   done
 
   864 
   951 
   865 lemma zzz' :
 
   952 (*lemma zzz' :
 
   866   "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))"
 
   953   "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))"
 
   867   using list_eq.intros(4) by (simp only: zzz)
 
   954   using list_eq.intros(4) by (simp only: zzz)
 
   868 
   955 
   869 thm QUOT_TYPE_I_fset.REPS_same
 
   956 thm QUOT_TYPE_I_fset.REPS_same
 
   870 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}
 
   957 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}
 
       
   958 *)
 
   871 
   959 
   872 thm list_eq.intros(5)
 
   960 thm list_eq.intros(5)
 
   873 ML {*
 
   961 ML {*
 
   874   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
 
   962   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
 
   875   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
 
   963   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
 
   876   val cgoal = cterm_of @{theory} goal
 
   964   val cgoal = cterm_of @{theory} goal
 
   877   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 
   965   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 
   878 *}
 
   966 *}
 
   879 prove {* Thm.term_of cgoal2 *}
 
   967 prove {* Thm.term_of cgoal2 *}
 
   880   apply (tactic {* transconv_fset_tac' @{context} *})
 
   968   apply (tactic {* transconv_fset_tac' @{context} *})
 
   909 
   997 
   910 definition
 
   998 definition
 
   911   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 
   999   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 
   912 where
 
  1000 where
 
   913   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
 
  1001   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
 
   914 
       
   915 (* TODO: Consider defining it with an "if"; sth like:
 
  1002 (* TODO: Consider defining it with an "if"; sth like:
 
   916    Babs p m = \<lambda>x. if x \<in> p then m x else undefined
 
  1003    Babs p m = \<lambda>x. if x \<in> p then m x else undefined
 
   917 *)
 
  1004 *)
 
   918 
       
   919 ML {*
 
       
   920 fun needs_lift (rty as Type (rty_s, _)) ty =
 
       
   921   case ty of
 
       
   922     Type (s, tys) =>
 
       
   923       (s = rty_s) orelse (exists (needs_lift rty) tys)
 
       
   924   | _ => false
 
       
   925 
       
   926 *}
 
       
   927 
  1005 
   928 ML {*
 
  1006 ML {*
 
   929 (* trm \<Rightarrow> new_trm *)
 
  1007 (* trm \<Rightarrow> new_trm *)
 
   930 fun regularise trm rty rel lthy =
 
  1008 fun regularise trm rty rel lthy =
 
   931   case trm of
 
  1009   case trm of
 
  1044   trm == new_trm
 
  1122   trm == new_trm
 
  1045 *)
 
  1123 *)
 
  1046 
  1124 
  1047 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *}
 
  1125 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *}
 
  1048 
  1126 
  1049 prove {*
 
  1127 prove list_induct_r: {*
 
  1050  Logic.mk_implies
 
  1128  Logic.mk_implies
 
  1051    ((prop_of li),
 
  1129    ((prop_of li),
 
  1052    (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
 
  1130    (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
 
  1053   apply (simp only: equiv_res_forall[OF equiv_list_eq])
 
  1131   apply (simp only: equiv_res_forall[OF equiv_list_eq])
 
  1054   thm RIGHT_RES_FORALL_REGULAR
 
  1132   thm RIGHT_RES_FORALL_REGULAR
 
  1056   prefer 2
 
  1134   prefer 2
 
  1057   apply (assumption)
 
  1135   apply (assumption)
 
  1058   apply (metis)
 
  1136   apply (metis)
 
  1059   done
 
  1137   done
 
  1060 
  1138 
       
  1139 ML {* val thm = @{thm list_induct_r} OF [li] *}
 
       
  1140 ML {* val trm = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 
       
  1141 ML {* Syntax.string_of_term @{context} trm |> writeln *}
 
       
  1142 term fun_map
 
       
  1143 ML {* Toplevel.program (fn () => cterm_of @{theory} trm) *}
 
       
  1144 
  1061 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
 
  1145 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
 
  1062 
  1146 
  1063 prove card1_suc_r: {*
 
  1147 prove card1_suc_r: {*
 
  1064  Logic.mk_implies
 
  1148  Logic.mk_implies
 
  1065    ((prop_of card1_suc_f),
 
  1149    ((prop_of card1_suc_f),
 
  1084 *}
 
  1168 *}
 
  1085 
  1169 
  1086 ML {*
 
  1170 ML {*
 
  1087   val goal =
 
  1171   val goal =
 
  1088     Toplevel.program (fn () =>
 
  1172     Toplevel.program (fn () =>
 
  1089       build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
 
  1173       build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
 
  1090     )
 
  1174     )
 
  1091 *}
 
  1175 *}
 
  1092 ML {*
 
  1176 ML {*
 
  1093   val cgoal = 
  1177   val cgoal =
 
  1094     Toplevel.program (fn () =>
 
  1178     Toplevel.program (fn () =>
 
  1095       cterm_of @{theory} goal
 
  1179       cterm_of @{theory} goal
 
  1096     )
 
  1180     )
 
  1097   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 
  1181   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 
  1098 *}
 
  1182 *}
nominal2